The CNF Encoding Complexity of Boolean Functions
September 16, 2026 (GHC 6501)
How many clauses does it take to encode a Boolean function in CNF, allowing auxiliary variables? A partial answer is given by the efficient Cook-Levin-Robson theorems: if the function can be computed in time T, then O(T lg T) clauses suffice. It turns out in many cases we can do much better! I will give a tour of the fascinating world of compact CNF encodings, and in particular, I will present a non-uniform version of Cook-Levin-Robson: a function computable in time T by a non-deterministic RAM machine with access to M bits of advice can be encoded in roughly T + sqrt{MT} clauses.